finite($T$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$f$:($T$$\rightarrow$$T$). Inj($T$; $T$; $f$) $\Rightarrow$ Surj($T$; $T$; $f$)